\begin{tabbing}
sys{-}order(${\it es}$; ${\it Sys}$; $f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$a_{1}$, $b_{1}$:E(${\it Sys}$).\+
\\[0ex]$a_{1}$ is $f$$\ast$($b_{1}$)
\\[0ex]$\Rightarrow$ \=($\forall$$a_{2}$, $b_{2}$:E(${\it Sys}$).\+
\\[0ex]$a_{2}$ is $f$$\ast$($b_{2}$)
\\[0ex]$\Rightarrow$ ($a_{1}$ $<$loc $a_{2}$)
\\[0ex]$\Rightarrow$ ($\neg$$a_{1}$ is $f$$\ast$($a_{2}$))
\\[0ex]$\Rightarrow$ (loc($b_{1}$) = loc($b_{2}$))
\\[0ex]$\Rightarrow$ ($b_{1}$ $<$loc $b_{2}$))
\-\-
\end{tabbing}